a:. a | 1  (a ~ 1) 

latex

Definitions	a ~ b, P  Q, P  Q, P  Q, P & Q, Prop, b | a, x:A. B(x), t  T
Lemmas	one divs any, divides wf